| Definitions |  es.P(es),  x.A(x),  x. t(x), let x,y = A in B(x;y), {x:A| B(x)} ,  , E, t.1, x when e, R-Feasible(R), es realizer ind, Atom$n, EqDecider(T), EOrderAxioms(E; pred?; info), IdLnk, type List, Msg(M), left + right, Unit,  , val-axiom(E;V;M;info;pred?;init;Trans;Choose;Send;val;time), r  s, e < e',  , Top, P & Q, Knd, kindcase(k; a.f(a); l,t.g(l;t) ), Type, constant_function(f;A;B),  A,  b, <a, b>, loc(e), SWellFounded(R(x;y)), pred!(e;e'), t  T,  , Id, EState(T), f(a),  x:A. B(x), ES, P   Q, A c B, x:A  B(x), e@i. P(e), s = t, vartype(i;x), x:A  B(x), Consistent(R;es), @i x initially v:T, "$x", es-realizer(p), init-p-realizable, A  B, constR{$x:ut2}(T; c; i), inl x , [car / cdr], Rframe(loc;T;x;L), [], Rinit(loc;T;x;v), Realizer, rec(x.A(x)), DeclaredType(ds;x), a:A fp B(a), FinProbSpace, State(ds),  , {i..j }, False, Void, #$n, i j < k, A B, a < b, l[i], i z j, i <z j, hd(l), @i(x:T), @i always.P(x), {T}, P  Q, P Q, a = b, (x after e), loc(e), @i only events in L change x : T, frame-p-realizable, Normal(T), tl(l), (x l), kind(e) |